This paper extends the dual calculus with inductive types and coinductivetypes. The paper first introduces a non-deterministic dual calculus withinductive and coinductive types. Besides the same duality of the original dualcalculus, it has the duality of inductive and coinductive types, that is, theduality of terms and coterms for inductive and coinductive types, and theduality of their reduction rules. Its strong normalization is also proved,which is shown by translating it into a second-order dual calculus. The strongnormalization of the second-order dual calculus is proved by translating itinto the second-order symmetric lambda calculus. This paper then introduces acall-by-value system and a call-by-name system of the dual calculus withinductive and coinductive types, and shows the duality of call-by-value andcall-by-name, their Church-Rosser properties, and their strong normalization.Their strong normalization is proved by translating them into thenon-deterministic dual calculus with inductive and coinductive types.
展开▼
